package sve;

import java.util.AbstractCollection;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.Iterator;

import xadd.XADD;
import xadd.XADD.BoolDec;
import cmdp.HierarchicalParser;

public class Buffer {

	private ArrayList<String> _boolVars;
	private HashMap<String, Integer> _varIds;
	private HashMap<String, Integer> _deltaIds;
	private XADD _xadd_context;

	public XADD getContext() {
		return _xadd_context;
	}

	public HashMap<String, Integer> getVarIds() {
		return _varIds;
	}

	public HashMap<String, Integer> getDeltaIds() {
		return _deltaIds;
	}

	public ArrayList<String> getBoolVars() {
		return _boolVars;
	}

	public boolean isBoolean(String var) {
		return _boolVars.contains(var);
	}

	public boolean checkIntegrity() {
		for (String var : _varIds.keySet()) {
			if (!isContainedInVars(var)) {
				exit("Unreferenced variable " + var + "! Check your input file");
				return false;
			}
		}

		return true;
	}

	public int getVar(String var) {
		int id = getId(var);
		if (id < 0) {
			id = getDeltaId(var);
		}

		return id;
	}

	private boolean isContainedInVars(String var) {
		int id = -1;
		for (String v : getCaseswithDeltas()) {
			// if (((id = getId(v)) > 0 && Utils.contains(var, _xadd_context.collectVars(id)))
			// || ((id = getDeltaId(v)) > 0 && Utils.contains(var, _xadd_context.collectVars(getDeltaId(v))))) {
			if (getVarId(v) > 0) {
				return true;
			}
		}
		return false;
	}

	private ArrayList<String> getCaseswithDeltas() {
		ArrayList<String> a = new ArrayList<String>();
		a.addAll(getVarIds().keySet());
		a.addAll(getDeltaIds().keySet());

		return a;
	}

	public Buffer(ArrayList input) {
		_boolVars = new ArrayList<String>();
		_varIds = new HashMap<String, Integer>();
		_deltaIds = new HashMap<String, Integer>();

		if (input == null) {
			System.out.println("Empty input file!");
			System.exit(1);
		}

		// take care of booleans :D
		buildXADDs(input);
		for (String s : _varIds.keySet()) {
			_originalIds.put(s, _varIds.get(s));
		}

		for (String s : _deltaIds.keySet()) {
			_originalIds.put(s, _deltaIds.get(s));
		}
	}

	public static Buffer parse(String filepath) {
		return new Buffer(HierarchicalParser.ParseFile(filepath));
	}

	private void buildXADDs(ArrayList input) {
		_xadd_context = new XADD();

		if (input == null) {
			System.out.println("Empty input file!");
			System.exit(1);
		}

		Iterator i = input.iterator();
		Object o;

		// Set up variables

		o = i.next();
		if (!(o instanceof String) || !((String) o).equalsIgnoreCase("bvariables")) {
			exit("Missing bvariable declarations: " + o);
		}
		// TODO: Add all boolean vars to XADD

		o = i.next();
		_boolVars.addAll((Collection<? extends String>) o);
		for (String v : _boolVars) {
			_xadd_context.getVarIndex(_xadd_context.new BoolDec(v), true);
		}

		// // TODO: Add all intermediate boolean vars to XADD

		// Set up cases
		while (i.hasNext()) {
			o = i.next();
			if (!(o instanceof String) || !((String) o).equalsIgnoreCase("case")) {
				break;
			}

			// o == "cases"
			String aname = (String) i.next();
			System.out.println("case: " + aname);
			// HashMap<String, ArrayList> cpt_map = new HashMap<String, ArrayList>();

			o = i.next();
			while (!((String) o).equalsIgnoreCase("endcase")) {// endaction
				String v = (String) o;
				o = i.next();
				if (o instanceof String && ((String) o).equalsIgnoreCase("delta")) {
					o = i.next();
					int xadd = _xadd_context.buildCanonicalXADD(((ArrayList) o));
					_deltaIds.put(v, xadd);
					// Utils.print((List) o);
				} else {
					int xadd = _xadd_context.buildCanonicalXADD(((ArrayList) o));
					_varIds.put(v, xadd);
					if (isBoolean(v)) {
						int idx = _xadd_context.getVarIndex(_xadd_context.new BoolDec(v), true);
						int high_branch = xadd;
						int low_branch = _xadd_context.apply(_xadd_context.getTermNode(XADD.ONE), high_branch,
								XADD.MINUS);
						xadd = _xadd_context.getINode(idx, low_branch, high_branch);
						xadd = _xadd_context.makeCanonical(xadd);
					}
				}
				o = i.next();
			}
		}

		checkIntegrity();
	}

	private static void exit(String s) {
		new Exception(s).printStackTrace();
		System.exit(-1);
	}

	public ArrayList<ArrayList<Integer>> getRefFactors(String v) {
		ArrayList<Integer> cases = new ArrayList<Integer>();
		ArrayList<Integer> deltas = new ArrayList<Integer>();
		for (String key : getAllVars()) {
			int id = getId(key);
			if (id > 0 && _xadd_context.collectVars(id).contains(v)) {
				cases.add(id);
			}
			id = getDeltaId(key);
			if (id > 0 && _xadd_context.collectVars(id).contains(v)) {
				deltas.add(id);
			}
		}
		ArrayList<ArrayList<Integer>> a = new ArrayList<ArrayList<Integer>>();
		a.add(cases);
		a.add(deltas);

		return a;
	}

	public ArrayList<String> getAllVars() {
		ArrayList<String> al = new ArrayList<String>();
		al.addAll(_varIds.keySet());
		al.addAll(_deltaIds.keySet());

		return al;
	}

	public int getId(String var) {
		if (!_varIds.containsKey(var)) {
			return -1;
		}

		return _varIds.get(var);
	}

	public ArrayList<ArrayList<Integer>> getIds(String[] qu) {
		ArrayList<ArrayList<Integer>> ids = new ArrayList<ArrayList<Integer>>();
		ids.add(new ArrayList<Integer>());
		ids.add(new ArrayList<Integer>());

		if (qu != null) {
			for (String var : qu) {
				ids.get(0).add(getId(var));
				int d = getDeltaId(var);
				if (d >= 0)
					ids.get(1).add(d);
			}
		}

		return ids;
	}

	public int getDeltaId(String var) {
		if (!_deltaIds.containsKey(var)) {
			return -1;
		}
		return _deltaIds.get(var);
	}

	public ArrayList<ArrayList<Integer>> getRefFactors(String[] q) {
		ArrayList<ArrayList<Integer>> all = new ArrayList<ArrayList<Integer>>();
		all.add(new ArrayList<Integer>());
		all.add(new ArrayList<Integer>());
		for (String qq : q) {
			ArrayList<ArrayList<Integer>> a = getRefFactors(qq);
			all.get(0).addAll(a.get(0));
			all.get(1).addAll(a.get(1));
		}

		return all;
	}

	public int getVarId(String var) {
		return getId(var) > 0 ? getId(var) : getDeltaId(var);
	}

	public String addVar(int qID) {
		String v = "_" + qID;
		_varIds.put(v, qID);
		return v;
	}

	public void removeVar(String var) {
		_varIds.remove(var);
	}

	public void removeVar(int id) {
		for (String s : _varIds.keySet()) {
			if (getVarId(s) == id) {
				removeVar(s);
				return;
			}
		}
	}

	public String getVar(int varId) {
		for (String var : _varIds.keySet()) {
			if (getVar(var) == varId) {
				return var;
			}
		}
		return "";
	}

	public void updateVar(String var, int qID) {
		int id = getVarId(var);
		if (id > 0) {
			_originalIds.put(var, id);
			_varIds.put(var, qID);
		} else if ((id = getDeltaId(var)) > 0) {
			_originalIds.put(var, id);
			_deltaIds.put(var, qID);
		}
	}

	private HashMap<String, Integer> _originalIds = new HashMap<String, Integer>();

	public ArrayList<String> getRefVariablesInOriginalNet(String var) {
		ArrayList<String> s = new ArrayList<String>();

		for (String v : _originalIds.keySet()) {
			if (!v.equals(var) && _xadd_context.collectVars(_originalIds.get(v)).contains(var)) {
				s.add(v);
			}
		}

		// for (String v : _originalIds.keySet()) {
		// if (!s.contains(v) && !v.equals(var) && _xadd_context.collectVars(getVar(v)).contains(var)) {
		// s.add(v);
		// }
		// }

		return s;
	}

	public AbstractCollection<String> collectOriginalVars(String var) {
		return _xadd_context.collectVars(_originalIds.get(var));
	}

	public boolean isDeltaId(int id) {
		return _deltaIds.containsValue(id);
	}
}
